⊢ { a = 1 } with a.b = 2

Error: You can only combine records

Explanation: You can combine records using the ❰⫽❱ operator, like this:


    ┌───────────────────────────────────────────┐
    │ { foo = 1, bar = "ABC" } ⫽ { baz = True } │
    └───────────────────────────────────────────┘


    ┌─────────────────────────────────────────────┐
    │ λ(r : { foo : Bool }) → r ⫽ { bar = "ABC" } │
    └─────────────────────────────────────────────┘


... but you cannot combine values that are not records.

For example, the following expressions are not valid:


    ┌──────────────────────────────┐
    │ { foo = 1, bar = "ABC" } ⫽ 1 │
    └──────────────────────────────┘
                                 ⇧
                                 Invalid: Not a record


    ┌───────────────────────────────────────────┐
    │ { foo = 1, bar = "ABC" } ⫽ { baz : Bool } │
    └───────────────────────────────────────────┘
                                 ⇧
                                 Invalid: This is a record type and not a record


    ┌───────────────────────────────────────────┐
    │ { foo = 1, bar = "ABC" } ⫽ < baz : Bool > │
    └───────────────────────────────────────────┘
                                 ⇧
                                 Invalid: This is a union type and not a record


You tried to combine the following value:

↳ { a = 1 }.a

... which is not a record, but is actually a:

↳ Natural

────────────────────────────────────────────────────────────────────────────────

1│ { a = 1 } with a.b = 2

(stdin):1:1